(** ** Funtions of list *)
Require Export List.
Require Export Matrix.Mat_def.
Import ListNotations.


Section list_functions.

Variable A:Set.
Variable Zero:A.
Variable negative:A->A.
Variable add:A->A->A.
Variable sub:A->A->A.
Variable mul:A->A->A.
Variable f1:A->A->A.

(* ################################################################# *)
(** * Definition of Functions of List *)

(** These functions help to implement matrix processing functions. *)

Section list_fun.

(** ** List Extraction Functions *)

(** Here are simple functions for extracting the first and tail
    components of a list. *)

(** *** nil_list *)
(** nil_list m = [nil;nil;...；nil],of which the length is m. *)
(*创建一个长度为m的nil空list*)
Fixpoint nil_list(m:nat): (list (list A)) :=
  match m with
  |O => nil
  |S n => nil::(nil_list n)
  end.

(** ** List Operation Functions *)

(** *** list_map *)
(** Perform a function mapping on each element in the list :
    [x1;x2;...;xn] -> [f x1;f x2;...;f xn]. **)

(*每个元素分别映射*)

Fixpoint list_map (f:A->A)(l:list A): list A :=
  match l  with
  | cons x x' => f x :: (list_map f x')
  | _ => nil
  end.

Print list.
(*
Inductive list (A : Type) : Type :=  nil : list A | cons : A -> list A -> list A
*)

(** *** list_each *)
(** Perform a function operation on each element in the two lists :
    f [x1;x2;...;xn]  [y1,y2,...,yn] -> [f x1 y1; f x2 y2;...;f xn yn]. *)

Fixpoint list_each (f:A->A->A)(l1:list A) (l2:list A): list A :=
  match l1,l2 with
    hd1::tl1,hd2::tl2 => f hd1 hd2 ::(list_each f tl1 tl2 )
  | _,_ => nil
  end.

(** *** product'  *)(*乘积*)
(** Product of two lists: 
    [x1;x2;...;xn] * [y1;y2;..;yn] = x1*y1+x2*y2+...+xn*yn.  *)

Fixpoint product'(l1 l2:list A) :=
  match l1 , l2 with
    | h1::t1,h2::t2 => add (mul h1 h2) (product' t1 t2)
    | _ ,_ => Zero
  end.

End list_fun.

(** * Reasoning About List *)

(** The properties of these functions helps us to prove the properties
    of the matrix. *)

Section list_lemma.

(** ** Reasoning About List Transformation Functions *)

(** *** list_add *)
(*app是将表与表连接*)
(*::是将元素与表连接,a::l中，a是一维表作为元素，l是二维表是作为表*)
Lemma list_app: forall (a:list A) (l:list(list A)) , [a] ++ l = a :: l.
Proof.
  induction a.
  - simpl. auto.
  - simpl. auto.
Qed.

(** *** width_cons *)
(** If the width of the two-dimensional list a::l is n, then the length
    of list a is n and the width of l is n. *)
Lemma width_cons : forall (a:list A) ll n, 
  width (a :: ll) n ->length a = n/\width  ll n.
Proof.
  intros a.
  induction ll.
  induction n.
  - simpl. intros. destruct H. auto.
  - simpl. intros. destruct H. auto.
  - induction n.
    + simpl. intros. destruct H. auto.
    + simpl. intros. destruct H. auto.
Qed.

(** *** In_length *)
(** If the width of the two-dimensional list ma is n and l is one list
    of ma, then the length of l is n. *)
Lemma In_length: forall n l (ma:list(list A)),
  width ma n ->In l ma ->length l = n.
Proof.
  intros n l ma. generalize dependent n. generalize dependent l.
  induction ma as [|x ma' IHma'].
  - intros. induction n as[|n' IHn'].
    + simpl in H0. destruct H0. + simpl in H0. destruct H0.
  - intros. induction n as[|n' IHn'].
    + simpl in H. destruct H as [H1 H2].
      simpl in H0. destruct H0 as [H3|H4]. rewrite <- H3.
      apply H1. apply IHma'. apply H2. apply H4.
    + simpl in H. destruct H as [H1 H2].
      simpl in H0. destruct H0 as [H3|H4].
      rewrite <- H3. apply H1. apply IHma'. apply H2. apply H4.
Qed.

(** ** Reasoning About List Operation Functions *)

(** *** product'_comm *)
(** Lists product commutativity : l1*l2 = l2*l1. *)
Lemma product'_comm : forall (l1 l2:list A) ,
   (forall a b, mul a b = mul b a ) ->
   product' l1 l2 = product' l2 l1.
Proof.
  induction l1.
  - intros. simpl. induction l2.
    + simpl. auto.
    + simpl. auto.
  - intros. induction l2.
    + simpl. auto.
    + simpl. rewrite H. f_equal. apply IHl1.
      apply H.
Qed.
(*
fun (A B : Type) (f : A -> B) (x y : A) (H : x = y) =>
  match H in (_ = y0) return (f x = f y0) with
    | eq_refl => eq_refl
  end.
等边两边相等，消去公共项
*)
Print f_equal.

Lemma product'_nil_r: forall l,
  product' l nil = Zero.
Proof.
  induction l. simpl. auto.
  simpl. auto.
Qed.

(** *** list_each_length *)
(** The length of the list obtained after a certain operation of the
    two list is unchanged. *)
Lemma list_each_length:forall n (l r:list A),
  length l = n -> length r = n -> length (list_each f1 l r) = n.
Proof.
  induction n.
  induction l.
  induction r.
  - simpl. auto.
  - simpl. auto.
  - intros. inversion H.
  - induction l. induction r.
    + simpl. intros. inversion H.
    + simpl. intros. inversion H.
    + induction r.
      { simpl. intros. inversion H0. }
      { simpl. intros. apply eq_S. apply IHn. auto. auto. }
Qed.

(** *** list_each_comm *)
(** List Operation Commutativity :
    f a b = f b a -> f l1 l2 = f l2 l1 *)
Lemma list_each_comm : forall n l1 l2,
  (forall a b, f1 a b = f1 b a)-> 
  length l1 = n -> length l2 = n -> 
  list_each f1 l1 l2 = list_each f1 l2 l1.
Proof.
  induction n.
  induction l1.
  induction l2.
  - simpl. auto.
  - simpl. auto.
  - induction l2.
    + simpl. auto.
    + simpl. intros. inversion H0.
  - induction l1.
    + induction l2.
      { simpl. auto. }
      { simpl. auto. }
    + induction l2.
      { simpl. auto. }
      { simpl. intros. f_equal. apply H. apply IHn;auto. }
Qed.

(** *** list_each_assoc *)
(** List Operation Associativity :
    f (f a b) c = f a (f b c)) ->f (f l1 l2) l3 = f l1 (f l2 l3)). *)
Lemma list_each_assoc: forall n l1 l2 l3 ,
  (forall a b c, f1 (f1 a b) c = f1 a (f1 b c)) ->
   length l1 = n -> length l2 = n -> length l3 = n -> 
  list_each f1 (list_each f1 l1 l2) l3 = list_each f1 l1 (list_each f1 l2 l3).
Proof.
  induction n.
  induction l1.
  induction l2.
  induction l3.
  - simpl. auto.
  - simpl. auto.
  - simpl. auto.
  - intros. inversion H0.
  - induction l1. induction l2. induction l3.
    + simpl. auto.
    + simpl. auto.
    + simpl. auto.
    + induction l2. induction l3.
      { simpl. auto. }
      { simpl. auto. }
      { induction l3.
        * simpl. auto.
        * simpl. intros. rewrite H. rewrite IHn. auto. auto. auto. auto. auto. }
Qed.

(** *** list_sub_opp *)
(** List substraction commutativity : 
    a-b = -(a-b) -> l1-l2 = -(l1-l2). *)
Lemma list_sub_opp : forall l1 l2 , 
  (forall a b, sub a b = negative (sub b a)) -> 
  list_each sub l1 l2 = list_map negative (list_each sub l2 l1).
Proof.
  induction l1.
  induction l2.
  - simpl. auto.
  - simpl. auto.
  - induction l2.
    + simpl. auto.
    + simpl. intros. f_equal. auto. apply IHl1. auto.
Qed.

(** *** list_sub_comm *) 
(** List substraction commutativity2 : 
    a-b-c = a-c-b -> l1-l2-l3 = l1-l3-l2. *)
Lemma list_sub_comm : forall l1 l2 l3,
  (forall a b c, sub (sub a b) c = sub (sub a c) b) -> 
  list_each sub (list_each sub l1 l2) l3 
    = list_each sub (list_each sub l1 l3) l2.
Proof.
  induction l1.
  - simpl. auto.
  - induction l2. induction l3.
    + simpl. auto.
    + simpl. auto.
    + induction l3.
      { simpl. auto. }
      { simpl. intros. f_equal. auto. apply IHl1. auto. }
Qed.

(** *** list_sub_assoc *)
(** List substraction associativity : 
    a-b-c = a-(b+c) -> l1-l2-l3 = l1-(l2+l3). *)
Lemma list_sub_assoc : forall l1 l2 l3 ,
  (forall a b c,sub (sub a b) c = sub a (add b c)) -> 
  list_each sub (list_each sub l1 l2) l3 
    = list_each sub l1 (list_each add l2 l3).
Proof.
  induction l1.
  - simpl. auto.
  - induction l2. induction l3.
    + simpl. auto.
    + simpl. auto.
    + induction l3.
      { simpl. auto. }
      { simpl. intros. f_equal. auto. apply IHl1. auto. }
Qed.

(** ** Lemmas of nil_list *)

(** *** height_nil_list *)
(** height [nil1;nil2;...nilm] = m. *)
Lemma height_nil_list : forall m,
  height (nil_list m) = m.
Proof.
  induction m.
  - simpl. reflexivity.
  - simpl. rewrite IHm. reflexivity.
Qed.

(** *** width_nil_list*)
(** The width of nil_list m equals to 0. *)
Lemma width_nil_list : forall m,
  width (nil_list m) 0.
Proof.
  induction m.
  - simpl. reflexivity.
  - simpl. split. reflexivity. apply IHm.
Qed.

Lemma S_right : forall m1 m2,
  m1 + S m2 = S m1 + m2.
Proof.
  induction m1. simpl. auto.
  induction m2. simpl. f_equal. auto.
  simpl. f_equal. rewrite IHm1. simpl. f_equal.
Qed. 

Lemma nil_list_app: forall m2 m1,
  nil_list (m1+m2) = (nil_list m1) ++ (nil_list m2).
Proof.
  induction m2. induction m1. simpl. auto.
  simpl. f_equal. apply IHm1. induction m1.
  simpl. auto. simpl. f_equal. apply IHm1.
Qed.

(** *** length_dlist_0 *)
(** If the height of a two-dimensional list ma equals to 0 ,then ma
    is nil *)
Lemma height_dlist_0: forall (ma:list(list A)) ,
  height ma = 0 -> ma = nil.
Proof.
  induction ma.
  - auto. - simpl. intros. discriminate H.
Qed.

(** *** width_dlist_0 *)
(** Two-dimensional list that satisfies height ma = m and 
    width ma 0 equals to nil_list with m *)
Lemma width_dlist_0 : forall m (ma:list(list A)),
  height ma = m -> width ma 0 -> ma = nil_list m.
Proof.
  induction m.
  - induction ma.
    + simpl. reflexivity.
    + intros. inversion H.
  - induction ma.
    + intros. inversion H.
    + intros. simpl. inversion H0. apply length_zero_iff_nil in H1.
      rewrite H1. f_equal. apply IHm. inversion H. reflexivity.
      apply H2.
Qed.

Fixpoint mapp(dl1 dl2:list(list A)):=
  match dl1 with
  |nil => dl2
  |x::x'=> match dl2 with
           | nil => dl1
           | y::y' => x::mapp x' dl2
           end
  end.

Lemma app_nil_r: forall (l:list A),
  app l [] = l.
Proof.
  induction l.
  simpl. auto. simpl. f_equal. apply IHl.
Qed.

Lemma length_app : forall m1 m2 (l1 l2:list A),
  length l1 = m1-> length l2 = m2 ->
  length(l1++l2) = m1+ m2.
Proof.
  induction m1. intros. apply length_zero_iff_nil in H.
  rewrite H. simpl. auto.
  induction m2. intros. apply length_zero_iff_nil in H0.
  rewrite H0. simpl. auto. rewrite app_nil_r. rewrite H.
  auto.
  induction l1. intros. inversion H. induction l2.
  intros. inversion H0. intros. simpl. f_equal.
  apply IHm1. inversion H. auto. apply H0.
Qed.

Lemma height_mapp: forall m1 m2 ma mb,
  height ma = m1 -> height mb = m2 ->
  height (mapp ma mb) = m1+m2.
Proof.
  induction m1. induction m2. intros.
  apply length_zero_iff_nil in H. rewrite H. 
  apply length_zero_iff_nil in H0. rewrite H0.
  simpl. auto. induction ma. induction mb. intros.
  inversion H0. intros. simpl. f_equal. inversion H0.
  auto. intros. inversion H.
  induction m2. induction ma. intros. inversion H.
  induction mb. intros. simpl. f_equal. inversion H.
  auto. intros. inversion H0.  
  induction ma. intros. inversion H. induction mb.
  intros. inversion H0. intros. simpl.
  f_equal. apply IHm1. inversion H. auto. auto.
Qed.

Lemma width_mapp: forall n2 ma mb,
  width ma n2 -> width mb n2 ->
  width( mapp ma mb) n2.
Proof.
  induction n2. induction ma. induction mb. simpl. auto.
  simpl. auto. induction mb. simpl. auto. simpl.
  split. apply H. apply IHma. apply H. apply H0.
  induction ma. induction mb. simpl. auto.
  simpl. auto. induction mb. intros. apply H. intros.
  simpl. split. apply H. apply IHma. apply H. apply H0.
Qed.

Lemma nil_list_mapp: forall m2 m1,
  nil_list (m1+m2) = mapp (nil_list m1) (nil_list m2).
Proof.
  induction m2. induction m1. simpl. auto.
  simpl. f_equal. f_equal. auto. induction m1.
  simpl. auto. simpl. f_equal. apply IHm1.
Qed.

Lemma cons_app: forall a (ma mb:list A),
  a:: ma ++ mb = (a::ma)++mb.
Proof.
  - induction ma. * simpl. auto. * induction mb.
    rewrite ?app_nil_r. auto. simpl. auto.
Qed.

Lemma S_plus_1: forall m,
  m+1 = S m.
Proof.
  induction m. auto.
  simpl. f_equal. auto.
Qed.

Lemma rev_nil_list: forall m,
  rev(nil_list m ) = nil_list  m.
Proof.
  induction m. simpl. auto.
  simpl. rewrite IHm. assert(nil :: nil = nil_list  1).
  { auto. } rewrite H. rewrite <- nil_list_app.
  assert(nil :: nil_list  m =nil_list  (S m)).
  { simpl. auto. } rewrite H0. f_equal. apply S_plus_1.
Qed.

Lemma length_rev: forall m (ma:list A),
  length ma = m -> length( rev ma) = m.
Proof.
  induction m. induction ma. simpl. auto.
  intros. inversion H. induction ma. intros. inversion H.
  intros. simpl. rewrite <-S_plus_1. rewrite length_app with(m1:=m)(m2:=1).
  auto. apply IHm. inversion H. auto. auto.
Qed.

Lemma cons_rev: forall l (ma:list A),
  l::rev ma = rev(ma++l::nil).
Proof.
  induction ma. simpl. auto.
  simpl. rewrite <-IHma. auto.
Qed.

Lemma app_assoc: forall (ma mb mc:list A),
  (ma ++ mb)++mc = ma++(mb++mc).
Proof.
  induction ma. simpl. auto.
  induction mb. simpl. rewrite app_nil_r. auto.
  induction mc. rewrite ?app_nil_r. auto.
  simpl. f_equal. rewrite IHma. auto.
Qed.

Lemma rev_app: forall (ma mb:list A),
  rev (ma++mb) = (rev mb)++(rev ma).
Proof.
  induction ma. simpl. intros. rewrite app_nil_r. auto.
  induction mb. simpl. rewrite app_nil_r. auto.
  simpl. rewrite IHma. simpl. rewrite app_assoc.
  auto.
Qed.

End list_lemma.

End list_functions.